課程名稱 |
程式語言:命令程式設計 Programming Languages: Imperative Program Construction |
開課學期 |
110-1 |
授課對象 |
管理學院 資訊管理學系 |
授課教師 |
穆信成 |
課號 |
IM2013 |
課程識別碼 |
705 20700 |
班次 |
|
學分 |
3.0 |
全/半年 |
半年 |
必/選修 |
選修 |
上課時間 |
星期四2,3,4(9:10~12:10) |
上課地點 |
管一101 |
備註 |
總人數上限:79人 外系人數限制:10人 |
Ceiba 課程網頁 |
http://ceiba.ntu.edu.tw/1101IM2013_ |
課程簡介影片 |
|
核心能力關聯 |
核心能力與課程規劃關聯圖 |
課程大綱
|
為確保您我的權利,請尊重智慧財產權及不得非法影印
|
課程概述 |
欲知更詳盡資料請參考課程網頁:
https://scmu.github.io/plip/
本課程第一至第三週預計採用 Webex 線上開課,URL 如下:
https://ntumeet.webex.com/ntumeet/j.php?MTID=meb4d67fe0dc40e4888ea8d64d1ba5475
已修課、正考慮修課、或欲旁聽之同學可於上課時間連線至該 URL 聽課。建議稍加提前,以處理技術問題。
====================================================================
「命令」(imperative) 程式語言意指把程式視為「給電腦一個個指令」的語言。我們常用的 C, Python, Java 等語言都可歸屬在此類別下。這類程式語言中,該怎麼寫程式、該怎麼證明程式的正確性?
本課程為「程式語言(Programming Languages)」系列課程之一,著眼點並不是教特定程式語言,而是討論設計程式解決問題的思考方式、設計程式使用的數學與邏輯基礎、以及程式語言與形式符號在其中扮演的角色。本課程以命令程式為主角,其核心概念包括:
* 程式語言是一種形式語言,作為思考的工具。我們用程式語言表達概念,也用程式語言中的形式規則檢驗程式的正確性。
*「寫程式」不只是把程式碼生出來的動作 --- 我們還得確定程式是「對」的。而確定程式正確的唯一方法是證明。
* 「程式推導」:由問題的規格開始,一邊推導出解決該問題的程式,一邊做該程式為何正確的證明。
* 當我們不知一個程式該怎麼寫,「這個程式該怎麼證明」這件事可以反過來透露一些「這個程式該怎麼寫」的提示。
* 「寫程式」是一個數學行為。
* 為了討論使用指標的程式,我們發明了相對應的「分離邏輯」,藉以證明這類程式的正確性。
本課程將討論的具體工具包括
* Dijkstra 的 Guarded Command Language.
* 命題邏輯 (propositional logic)、一階邏輯 (first-order logic)
* Hoare Logic.
* The "weakest precondition" predicate transformer.
* Separation logic.
本課程與「程式語言:函數程式設計」有可呼應之處,但兩者都可獨立修習。本課程亦與「軟體規格與驗證(Software Specification and Verification)」非常相關:命題邏輯、Hoare Logic, predicate transformer 等都是兩堂課共同的元素。該課程談驗證 (verification), 本課程則較注重推導(derivation),有較多手動計算與演算法問題的推導,而不會嚴謹地談到語意、函數呼叫、concurrency 等課題。 |
課程目標 |
將嚴謹的、形式化的邏輯思考帶入程式設計中。訓練學生由問題的規格開始,一邊推導出解決該問題的程式,一邊做該程式為何正確的證明。由此培養對於程式正確性的要求、對於「程式設計是什麼」提出一個不同的觀點。
|
課程要求 |
本課程並非程式設計入門課程。適合選修本課程之學生應:
* 能以指令式語言(C, Java, Python... etc)撰寫簡單的程式,對此類語言的控制結構有基本熟悉度,
* 有基本數學能力,對用紙筆進行的算式演算不會恐懼,
* 對於以形式邏輯思考解決問題、用數學方法證明程式的正確性有興趣。 |
預期每週課後學習時數 |
|
Office Hours |
|
指定閱讀 |
待補 |
參考書目 |
Backhouse, Roland. Program Construction: Calculating Implementations from Specifications. Wiley, 2003.
Dijkstra, Edsger W. A Discipline of Programming. Prentice Hall, 1976.
Dijkstra, Edsger W. and Scholten, Carel S. Predicate Calculus and Program Semantics. Springer-Verlag, 1990.
Gries, David. The Science of Programming. Springer-Verlag, 1981.
Kaldewaij, Anne. Programming - the Derivation of Algorithms. Prentice Hall, 1990.
Morgan, Carroll. Programming from Specifications, Second Edition. Prentice Hall, 1994. |
評量方式 (僅供參考) |
No. |
項目 |
百分比 |
說明 |
1. |
期中考 |
50% |
僅採計期中考、期末考成績,比率機動調整(例:高分者60%, 低分者40%)。課堂中將發習題,但不計入學期分數。出席不計。
|
2. |
期末考 |
50% |
僅採計期中考、期末考成績,比率機動調整(例:高分者60%, 低分者40%)。課堂中將發習題,但不計入學期分數。出席不計。
|
|
週次 |
日期 |
單元主題 |
第1週 |
9/23 |
概論 Overview
Guarded Command Language, Hoare Logic, and Weakest Precondition.
-- 設值、條件判斷 Assignment, Conditional Branching. |
第2週 |
9/30 |
Guarded Command Language, Hoare Logic, and Weakest Precondition.
-- 迴圈與恆式 Loops and Loop Invariants. |
第3週 |
10/07 |
簡易程式推導 Simple Program Derivation.
-- 最弱前提 Weakest Precondition.
-- 設值與代換 Assignment and Substitutions
-- 條件程式推導 Branching Derivation |
第4週 |
10/14 |
迴圈建構一般技巧 General Loop Construction
-- 由合取中提出恆式 Conjuncts as Invariants. |
第5週 |
10/21 |
迴圈建構一般技巧 General Loop Construction.
-- 增強恆式 Strengthening the Invariant. |
第6週 |
10/28 |
迴圈建構一般技巧 General Loop Construction.
-- 使用遞移律的恆式 Associative Invariants. |
第7週 |
11/04 |
延續上週主題。 |
第8週 |
11/11 |
期中考 |
第9週 |
11/18 |
Case Study.
-- 二元搜尋 Binary Search. |
第10週 |
11/25 |
Case Study.
-- 有界線性搜尋 Bounded Linear Search. |
第11週 |
12/02 |
Case Study. |
第12週 |
12/09 |
Case Study. |
第13週 |
12/16 |
分離邏輯 Separation Logic. |
第14週 |
12/23 |
分離邏輯 Separation Logic. |
第15週 |
12/30 |
分離邏輯 Separation Logic. |
第16週 |
1/06 |
期末考 |
|